COMMENT ⊗   VALID 00002 PAGES 
RECORD PAGE   DESCRIPTION
 00001 00001
 00002 00002	.BEGIN DOUBLE SPACE
 00008 ENDMK
⊗;
.BEGIN DOUBLE SPACE
A simple language has been devised for more precise descriptions of 
strategies than Boolean combinations of the builtin strategies.
This language is also useful for describing patterns for searching clause
lists using FIND and FINDC.

This language allows rather arbitrary functions on the syntactic structure 
of clauses terms and literal.
It is also expandable to handle semantic characterizations.

The  legal variables are of three sorts: clauses literals and terms.
The interpretation of the constructed formulas differs depending on whether
the formula is an editing strategy, a choice strategy, or a pattern.
Formulas  to be used for choice strategies are supposed to be applied
to a binary rule of inference, I, in the presence of two clauses, C1 and C2;
that is, I(C1,C2).
An editing strategy formula is to be applied to a single clause, thus there
should be exactly one `clause variable', currently named C.
Thus when we give choice strategies then formula is used as a filter on each
candidate; when we use the formulas on clause-lists in the editing phase, they
are to be `mapcar'ed .

Literal and term variables are designated by l1,l2,l3,...and t1,t2,t3,....

All quantifiers are implicitly relativized. E.g.
∀l1∃t2... means for every literal in the current clause there is a term in l1
such that...


PRIMITIVES:

1) ancestry	TR(x)

If x is clause c, then TR(x) gives the ancestry.
If x is either a literal or a term --l or t-- then TR(x) gives the structure of x.

Examples:

If x is an initial clauses then TR(x) is NIL. If x is a deduction then TR gives
a  list of the clauses appearing in the derivation tree.

2) length		α(x)

If x is a clause then α(x) gives the usual length--number of literals.
If x is a literal or term then α(x) gives the number of symbols which appear

Examples:

α(c)=1 is true if c is a unit-clause.

3) depth		∂(x)

If x is a clause, then ∂(x) gives the depth of the derivation tree.
If x is a literal or term then ∂(x) gives the depth of function-nesting.
.END

.BEGIN VERBATIM

PREDICATES:

=,<,>,≠,¬	equality,less-than,greater-than,not-equal, not
∧,∨,ε		and,or,clever membership.
[ p→e; ...]	conditionals

.END

.BEGIN DOUBLE SPACE

Examples:
a) ∂(t1)<5 ∧TR(c)=NIL

Depth of nesting is less than 5 and clause is initial.

b) [α(c)=1 → ∀l1 E(_,_)εTR(l1) ; T → ∀l1 ¬ -εTR(l1)]

   If clause is unit the the predicate, E, must appear; otherwise every literal
   in c must be positive.

MATCHING:

+,-		sign of a literal
⊂,⊃		set delimiters for and-membership
⊃,⊂		set delimiters for or-membershit

Examples;
⊂2,3,4⊃εTR(c)

   Each clause 2,3,and 4 must appear in the tree of c.

⊃2,3,4⊂εTR(c)

   At least one of these clauses must appeaar.

_		matches any term

x,y,z,u,v	used to match sub-terms.

Examples:
f(_,_) matches any occurrence of the function-letter,f.

f(g(x,_),_,x) matches any occurrence of f such that f's first position is
an occurrence of g; and g's first position matches the third position of f.

Examples:

Definition of some of the builtin strategies in the language.

.END

.BEGIN VERBATIM

ANCESTRY: 	TR(C1)=NIL ∨ TR(C2)=NIL ∨ C2εTR(C1) ∨ C1εTR(C2)
SUPPORT[...]:  	[TR(C2)=NIL → ⊃...⊂εTR(C2);T → T]
UNIT:  		α(C1)=1 ∨ α(C2)=1
VINE: 		TR(C1)=NIL ∨ TR(C2)=1

LENGTH[#]: 	α(C) > # 
DEPTH[#]: 	∂(C) > #

.END